ap2(ap2(map, f), xs) -> ap2(ap2(ap2(if, ap2(isEmpty, xs)), f), xs)
ap2(ap2(ap2(if, true), f), xs) -> nil
ap2(ap2(ap2(if, false), f), xs) -> ap2(ap2(cons, ap2(f, ap2(last, xs))), ap2(ap2(map, f), ap2(dropLast, xs)))
ap2(isEmpty, nil) -> true
ap2(isEmpty, ap2(ap2(cons, x), xs)) -> false
ap2(last, ap2(ap2(cons, x), nil)) -> x
ap2(last, ap2(ap2(cons, x), ap2(ap2(cons, y), ys))) -> ap2(last, ap2(ap2(cons, y), ys))
ap2(dropLast, nil) -> nil
ap2(dropLast, ap2(ap2(cons, x), nil)) -> nil
ap2(dropLast, ap2(ap2(cons, x), ap2(ap2(cons, y), ys))) -> ap2(ap2(cons, x), ap2(dropLast, ap2(ap2(cons, y), ys)))
↳ QTRS
↳ DependencyPairsProof
ap2(ap2(map, f), xs) -> ap2(ap2(ap2(if, ap2(isEmpty, xs)), f), xs)
ap2(ap2(ap2(if, true), f), xs) -> nil
ap2(ap2(ap2(if, false), f), xs) -> ap2(ap2(cons, ap2(f, ap2(last, xs))), ap2(ap2(map, f), ap2(dropLast, xs)))
ap2(isEmpty, nil) -> true
ap2(isEmpty, ap2(ap2(cons, x), xs)) -> false
ap2(last, ap2(ap2(cons, x), nil)) -> x
ap2(last, ap2(ap2(cons, x), ap2(ap2(cons, y), ys))) -> ap2(last, ap2(ap2(cons, y), ys))
ap2(dropLast, nil) -> nil
ap2(dropLast, ap2(ap2(cons, x), nil)) -> nil
ap2(dropLast, ap2(ap2(cons, x), ap2(ap2(cons, y), ys))) -> ap2(ap2(cons, x), ap2(dropLast, ap2(ap2(cons, y), ys)))
AP2(ap2(map, f), xs) -> AP2(ap2(if, ap2(isEmpty, xs)), f)
AP2(ap2(ap2(if, false), f), xs) -> AP2(last, xs)
AP2(ap2(ap2(if, false), f), xs) -> AP2(f, ap2(last, xs))
AP2(ap2(map, f), xs) -> AP2(if, ap2(isEmpty, xs))
AP2(ap2(ap2(if, false), f), xs) -> AP2(ap2(cons, ap2(f, ap2(last, xs))), ap2(ap2(map, f), ap2(dropLast, xs)))
AP2(ap2(map, f), xs) -> AP2(isEmpty, xs)
AP2(last, ap2(ap2(cons, x), ap2(ap2(cons, y), ys))) -> AP2(last, ap2(ap2(cons, y), ys))
AP2(ap2(ap2(if, false), f), xs) -> AP2(ap2(map, f), ap2(dropLast, xs))
AP2(ap2(map, f), xs) -> AP2(ap2(ap2(if, ap2(isEmpty, xs)), f), xs)
AP2(ap2(ap2(if, false), f), xs) -> AP2(map, f)
AP2(ap2(ap2(if, false), f), xs) -> AP2(cons, ap2(f, ap2(last, xs)))
AP2(dropLast, ap2(ap2(cons, x), ap2(ap2(cons, y), ys))) -> AP2(dropLast, ap2(ap2(cons, y), ys))
AP2(ap2(ap2(if, false), f), xs) -> AP2(dropLast, xs)
AP2(dropLast, ap2(ap2(cons, x), ap2(ap2(cons, y), ys))) -> AP2(ap2(cons, x), ap2(dropLast, ap2(ap2(cons, y), ys)))
ap2(ap2(map, f), xs) -> ap2(ap2(ap2(if, ap2(isEmpty, xs)), f), xs)
ap2(ap2(ap2(if, true), f), xs) -> nil
ap2(ap2(ap2(if, false), f), xs) -> ap2(ap2(cons, ap2(f, ap2(last, xs))), ap2(ap2(map, f), ap2(dropLast, xs)))
ap2(isEmpty, nil) -> true
ap2(isEmpty, ap2(ap2(cons, x), xs)) -> false
ap2(last, ap2(ap2(cons, x), nil)) -> x
ap2(last, ap2(ap2(cons, x), ap2(ap2(cons, y), ys))) -> ap2(last, ap2(ap2(cons, y), ys))
ap2(dropLast, nil) -> nil
ap2(dropLast, ap2(ap2(cons, x), nil)) -> nil
ap2(dropLast, ap2(ap2(cons, x), ap2(ap2(cons, y), ys))) -> ap2(ap2(cons, x), ap2(dropLast, ap2(ap2(cons, y), ys)))
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
AP2(ap2(map, f), xs) -> AP2(ap2(if, ap2(isEmpty, xs)), f)
AP2(ap2(ap2(if, false), f), xs) -> AP2(last, xs)
AP2(ap2(ap2(if, false), f), xs) -> AP2(f, ap2(last, xs))
AP2(ap2(map, f), xs) -> AP2(if, ap2(isEmpty, xs))
AP2(ap2(ap2(if, false), f), xs) -> AP2(ap2(cons, ap2(f, ap2(last, xs))), ap2(ap2(map, f), ap2(dropLast, xs)))
AP2(ap2(map, f), xs) -> AP2(isEmpty, xs)
AP2(last, ap2(ap2(cons, x), ap2(ap2(cons, y), ys))) -> AP2(last, ap2(ap2(cons, y), ys))
AP2(ap2(ap2(if, false), f), xs) -> AP2(ap2(map, f), ap2(dropLast, xs))
AP2(ap2(map, f), xs) -> AP2(ap2(ap2(if, ap2(isEmpty, xs)), f), xs)
AP2(ap2(ap2(if, false), f), xs) -> AP2(map, f)
AP2(ap2(ap2(if, false), f), xs) -> AP2(cons, ap2(f, ap2(last, xs)))
AP2(dropLast, ap2(ap2(cons, x), ap2(ap2(cons, y), ys))) -> AP2(dropLast, ap2(ap2(cons, y), ys))
AP2(ap2(ap2(if, false), f), xs) -> AP2(dropLast, xs)
AP2(dropLast, ap2(ap2(cons, x), ap2(ap2(cons, y), ys))) -> AP2(ap2(cons, x), ap2(dropLast, ap2(ap2(cons, y), ys)))
ap2(ap2(map, f), xs) -> ap2(ap2(ap2(if, ap2(isEmpty, xs)), f), xs)
ap2(ap2(ap2(if, true), f), xs) -> nil
ap2(ap2(ap2(if, false), f), xs) -> ap2(ap2(cons, ap2(f, ap2(last, xs))), ap2(ap2(map, f), ap2(dropLast, xs)))
ap2(isEmpty, nil) -> true
ap2(isEmpty, ap2(ap2(cons, x), xs)) -> false
ap2(last, ap2(ap2(cons, x), nil)) -> x
ap2(last, ap2(ap2(cons, x), ap2(ap2(cons, y), ys))) -> ap2(last, ap2(ap2(cons, y), ys))
ap2(dropLast, nil) -> nil
ap2(dropLast, ap2(ap2(cons, x), nil)) -> nil
ap2(dropLast, ap2(ap2(cons, x), ap2(ap2(cons, y), ys))) -> ap2(ap2(cons, x), ap2(dropLast, ap2(ap2(cons, y), ys)))
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
↳ AND
↳ QDP
↳ QDPOrderProof
↳ QDP
↳ QDP
AP2(dropLast, ap2(ap2(cons, x), ap2(ap2(cons, y), ys))) -> AP2(dropLast, ap2(ap2(cons, y), ys))
ap2(ap2(map, f), xs) -> ap2(ap2(ap2(if, ap2(isEmpty, xs)), f), xs)
ap2(ap2(ap2(if, true), f), xs) -> nil
ap2(ap2(ap2(if, false), f), xs) -> ap2(ap2(cons, ap2(f, ap2(last, xs))), ap2(ap2(map, f), ap2(dropLast, xs)))
ap2(isEmpty, nil) -> true
ap2(isEmpty, ap2(ap2(cons, x), xs)) -> false
ap2(last, ap2(ap2(cons, x), nil)) -> x
ap2(last, ap2(ap2(cons, x), ap2(ap2(cons, y), ys))) -> ap2(last, ap2(ap2(cons, y), ys))
ap2(dropLast, nil) -> nil
ap2(dropLast, ap2(ap2(cons, x), nil)) -> nil
ap2(dropLast, ap2(ap2(cons, x), ap2(ap2(cons, y), ys))) -> ap2(ap2(cons, x), ap2(dropLast, ap2(ap2(cons, y), ys)))
The following pairs can be oriented strictly and are deleted.
The remaining pairs can at least be oriented weakly.
AP2(dropLast, ap2(ap2(cons, x), ap2(ap2(cons, y), ys))) -> AP2(dropLast, ap2(ap2(cons, y), ys))
POL( dropLast ) = 1
POL( ap2(x1, x2) ) = x1 + 3x2 + 3
POL( AP2(x1, x2) ) = max{0, 2x2 - 3}
POL( cons ) = 3
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
↳ AND
↳ QDP
↳ QDPOrderProof
↳ QDP
↳ PisEmptyProof
↳ QDP
↳ QDP
ap2(ap2(map, f), xs) -> ap2(ap2(ap2(if, ap2(isEmpty, xs)), f), xs)
ap2(ap2(ap2(if, true), f), xs) -> nil
ap2(ap2(ap2(if, false), f), xs) -> ap2(ap2(cons, ap2(f, ap2(last, xs))), ap2(ap2(map, f), ap2(dropLast, xs)))
ap2(isEmpty, nil) -> true
ap2(isEmpty, ap2(ap2(cons, x), xs)) -> false
ap2(last, ap2(ap2(cons, x), nil)) -> x
ap2(last, ap2(ap2(cons, x), ap2(ap2(cons, y), ys))) -> ap2(last, ap2(ap2(cons, y), ys))
ap2(dropLast, nil) -> nil
ap2(dropLast, ap2(ap2(cons, x), nil)) -> nil
ap2(dropLast, ap2(ap2(cons, x), ap2(ap2(cons, y), ys))) -> ap2(ap2(cons, x), ap2(dropLast, ap2(ap2(cons, y), ys)))
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
↳ AND
↳ QDP
↳ QDP
↳ QDPOrderProof
↳ QDP
AP2(last, ap2(ap2(cons, x), ap2(ap2(cons, y), ys))) -> AP2(last, ap2(ap2(cons, y), ys))
ap2(ap2(map, f), xs) -> ap2(ap2(ap2(if, ap2(isEmpty, xs)), f), xs)
ap2(ap2(ap2(if, true), f), xs) -> nil
ap2(ap2(ap2(if, false), f), xs) -> ap2(ap2(cons, ap2(f, ap2(last, xs))), ap2(ap2(map, f), ap2(dropLast, xs)))
ap2(isEmpty, nil) -> true
ap2(isEmpty, ap2(ap2(cons, x), xs)) -> false
ap2(last, ap2(ap2(cons, x), nil)) -> x
ap2(last, ap2(ap2(cons, x), ap2(ap2(cons, y), ys))) -> ap2(last, ap2(ap2(cons, y), ys))
ap2(dropLast, nil) -> nil
ap2(dropLast, ap2(ap2(cons, x), nil)) -> nil
ap2(dropLast, ap2(ap2(cons, x), ap2(ap2(cons, y), ys))) -> ap2(ap2(cons, x), ap2(dropLast, ap2(ap2(cons, y), ys)))
The following pairs can be oriented strictly and are deleted.
The remaining pairs can at least be oriented weakly.
AP2(last, ap2(ap2(cons, x), ap2(ap2(cons, y), ys))) -> AP2(last, ap2(ap2(cons, y), ys))
POL( last ) = 1
POL( ap2(x1, x2) ) = x1 + 3x2 + 3
POL( AP2(x1, x2) ) = max{0, 2x2 - 3}
POL( cons ) = 3
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
↳ AND
↳ QDP
↳ QDP
↳ QDPOrderProof
↳ QDP
↳ PisEmptyProof
↳ QDP
ap2(ap2(map, f), xs) -> ap2(ap2(ap2(if, ap2(isEmpty, xs)), f), xs)
ap2(ap2(ap2(if, true), f), xs) -> nil
ap2(ap2(ap2(if, false), f), xs) -> ap2(ap2(cons, ap2(f, ap2(last, xs))), ap2(ap2(map, f), ap2(dropLast, xs)))
ap2(isEmpty, nil) -> true
ap2(isEmpty, ap2(ap2(cons, x), xs)) -> false
ap2(last, ap2(ap2(cons, x), nil)) -> x
ap2(last, ap2(ap2(cons, x), ap2(ap2(cons, y), ys))) -> ap2(last, ap2(ap2(cons, y), ys))
ap2(dropLast, nil) -> nil
ap2(dropLast, ap2(ap2(cons, x), nil)) -> nil
ap2(dropLast, ap2(ap2(cons, x), ap2(ap2(cons, y), ys))) -> ap2(ap2(cons, x), ap2(dropLast, ap2(ap2(cons, y), ys)))
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
↳ AND
↳ QDP
↳ QDP
↳ QDP
↳ QDPOrderProof
AP2(ap2(ap2(if, false), f), xs) -> AP2(f, ap2(last, xs))
AP2(ap2(ap2(if, false), f), xs) -> AP2(ap2(map, f), ap2(dropLast, xs))
AP2(ap2(map, f), xs) -> AP2(ap2(ap2(if, ap2(isEmpty, xs)), f), xs)
ap2(ap2(map, f), xs) -> ap2(ap2(ap2(if, ap2(isEmpty, xs)), f), xs)
ap2(ap2(ap2(if, true), f), xs) -> nil
ap2(ap2(ap2(if, false), f), xs) -> ap2(ap2(cons, ap2(f, ap2(last, xs))), ap2(ap2(map, f), ap2(dropLast, xs)))
ap2(isEmpty, nil) -> true
ap2(isEmpty, ap2(ap2(cons, x), xs)) -> false
ap2(last, ap2(ap2(cons, x), nil)) -> x
ap2(last, ap2(ap2(cons, x), ap2(ap2(cons, y), ys))) -> ap2(last, ap2(ap2(cons, y), ys))
ap2(dropLast, nil) -> nil
ap2(dropLast, ap2(ap2(cons, x), nil)) -> nil
ap2(dropLast, ap2(ap2(cons, x), ap2(ap2(cons, y), ys))) -> ap2(ap2(cons, x), ap2(dropLast, ap2(ap2(cons, y), ys)))
The following pairs can be oriented strictly and are deleted.
The remaining pairs can at least be oriented weakly.
AP2(ap2(ap2(if, false), f), xs) -> AP2(f, ap2(last, xs))
Used ordering: Polynomial Order [17,21] with Interpretation:
AP2(ap2(ap2(if, false), f), xs) -> AP2(ap2(map, f), ap2(dropLast, xs))
AP2(ap2(map, f), xs) -> AP2(ap2(ap2(if, ap2(isEmpty, xs)), f), xs)
POL( true ) = 3
POL( dropLast ) = max{0, -3}
POL( last ) = 2
POL( AP2(x1, x2) ) = max{0, 2x1 - 3}
POL( false ) = max{0, -3}
POL( if ) = 3
POL( map ) = max{0, -3}
POL( ap2(x1, x2) ) = x2 + 2
POL( nil ) = max{0, -3}
POL( isEmpty ) = 3
POL( cons ) = 2
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
↳ AND
↳ QDP
↳ QDP
↳ QDP
↳ QDPOrderProof
↳ QDP
AP2(ap2(ap2(if, false), f), xs) -> AP2(ap2(map, f), ap2(dropLast, xs))
AP2(ap2(map, f), xs) -> AP2(ap2(ap2(if, ap2(isEmpty, xs)), f), xs)
ap2(ap2(map, f), xs) -> ap2(ap2(ap2(if, ap2(isEmpty, xs)), f), xs)
ap2(ap2(ap2(if, true), f), xs) -> nil
ap2(ap2(ap2(if, false), f), xs) -> ap2(ap2(cons, ap2(f, ap2(last, xs))), ap2(ap2(map, f), ap2(dropLast, xs)))
ap2(isEmpty, nil) -> true
ap2(isEmpty, ap2(ap2(cons, x), xs)) -> false
ap2(last, ap2(ap2(cons, x), nil)) -> x
ap2(last, ap2(ap2(cons, x), ap2(ap2(cons, y), ys))) -> ap2(last, ap2(ap2(cons, y), ys))
ap2(dropLast, nil) -> nil
ap2(dropLast, ap2(ap2(cons, x), nil)) -> nil
ap2(dropLast, ap2(ap2(cons, x), ap2(ap2(cons, y), ys))) -> ap2(ap2(cons, x), ap2(dropLast, ap2(ap2(cons, y), ys)))